DROPS

Document

DOI: 10.4230/LIPIcs.CSL.2024.19

Ehrenfeucht-Fraïssé Games in Semiring Semantics

Authors: Sophie Brinke, Erich Grädel, and Lovro Mrkonjić

Published in: LIPIcs, Volume 288, 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024)

Abstract

Ehrenfeucht-Fraïssé games provide a fundamental method for proving elementary equivalence (and equivalence up to a certain quantifier rank) of relational structures. We investigate the soundness and completeness of this method in the more general context of semiring semantics. Motivated originally by provenance analysis of database queries, semiring semantics evaluates logical statements not just by true or false, but by values in some commutative semiring; this can provide much more detailed information, for instance concerning the combinations of atomic facts that imply the truth of a statement, or practical information about evaluation costs, confidence scores, access levels or the number of successful evaluation strategies. There is a wide variety of different semirings that are relevant for provenance analysis, and the applicability of classical logical methods in semiring semantics may strongly depend on the algebraic properties of the underlying semiring. While Ehrenfeucht-Fraïssé games are sound and complete for logical equivalences in classical semantics, and thus on the Boolean semiring, this is in general not the case for other semirings. We provide a detailed analysis of the soundness and completeness of model comparison games on specific semirings, not just for classical Ehrenfeucht-Fraïssé games but also for other variants based on bijections or counting. Finally we propose a new kind of games, called homomorphism games, based on the fact that there exist locally very different semiring interpretations that can be proved to be elementarily equivalent via separating sets of homomorphisms. We prove that these homomorphism games provide a sound and complete method for logical equivalences on finite lattice semirings.

Cite as

Sophie Brinke, Erich Grädel, and Lovro Mrkonjić. Ehrenfeucht-Fraïssé Games in Semiring Semantics. In 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 288, pp. 19:1-19:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{brinke_et_al:LIPIcs.CSL.2024.19,
  author =	{Brinke, Sophie and Gr\"{a}del, Erich and Mrkonji\'{c}, Lovro},
  title =	{{Ehrenfeucht-Fra\"{i}ss\'{e} Games in Semiring Semantics}},
  booktitle =	{32nd EACSL Annual Conference on Computer Science Logic (CSL 2024)},
  pages =	{19:1--19:22},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-310-2},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{288},
  editor =	{Murano, Aniello and Silva, Alexandra},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2024.19},
  URN =		{urn:nbn:de:0030-drops-196623},
  doi =		{10.4230/LIPIcs.CSL.2024.19},
  annote =	{Keywords: Semiring semantics, elementary equivalence, Ehrenfeucht-Fra\"{i}ss\'{e} games}
}

Document

DOI: 10.4230/LIPIcs.MFCS.2023.20

Locality Theorems in Semiring Semantics

Authors: Clotilde Bizière, Erich Grädel, and Matthias Naaf

Published in: LIPIcs, Volume 272, 48th International Symposium on Mathematical Foundations of Computer Science (MFCS 2023)

Abstract

Semiring semantics of first-order logic generalises classical Boolean semantics by permitting truth values from a commutative semiring, which can model information such as costs or access restrictions. This raises the question to what extent classical model-theoretic properties still apply, and how this depends on the algebraic properties of the semiring. In this paper, we study this question for the classical locality theorems due to Hanf and Gaifman. We prove that Hanf’s locality theorem generalises to all semirings with idempotent operations, but fails for many non-idempotent semirings. We then consider Gaifman normal forms and show that for formulae with free variables, Gaifman’s theorem does not generalise beyond the Boolean semiring. Also for sentences, it fails in the natural semiring and the tropical semiring. Our main result, however, is a constructive proof of the existence of Gaifman normal forms for min-max and lattice semirings. The proof implies a stronger version of Gaifman’s classical theorem in Boolean semantics: every sentence has a Gaifman normal form which does not add negations.

Cite as

Clotilde Bizière, Erich Grädel, and Matthias Naaf. Locality Theorems in Semiring Semantics. In 48th International Symposium on Mathematical Foundations of Computer Science (MFCS 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 272, pp. 20:1-20:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{biziere_et_al:LIPIcs.MFCS.2023.20,
  author =	{Bizi\`{e}re, Clotilde and Gr\"{a}del, Erich and Naaf, Matthias},
  title =	{{Locality Theorems in Semiring Semantics}},
  booktitle =	{48th International Symposium on Mathematical Foundations of Computer Science (MFCS 2023)},
  pages =	{20:1--20:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-292-1},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{272},
  editor =	{Leroux, J\'{e}r\^{o}me and Lombardy, Sylvain and Peleg, David},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2023.20},
  URN =		{urn:nbn:de:0030-drops-185546},
  doi =		{10.4230/LIPIcs.MFCS.2023.20},
  annote =	{Keywords: Semiring semantics, Locality, First-order logic}
}

Document

DOI: 10.4230/DagRep.12.2.1

Logic and Random Discrete Structures (Dagstuhl Seminar 22061)

Authors: Erich Grädel, Phokion G. Kolaitis, Marc Noy, and Matthias Naaf

Published in: Dagstuhl Reports, Volume 12, Issue 2 (2022)

Abstract

This report documents the program and the outcomes of Dagstuhl Seminar 22061 "Logic and Random Discrete Structures". The main topic of this seminar has been the analysis of large random discrete structures, such as trees, graphs, or permutations, from the perspective of mathematical logic. It has brought together both experts and junior researchers from a number of different areas where logic and random structures play a role, with the goal to establish new connections between such areas and to encourage interactions between foundational research and different application areas, including probabilistic databases.

Cite as

Erich Grädel, Phokion G. Kolaitis, Marc Noy, and Matthias Naaf. Logic and Random Discrete Structures (Dagstuhl Seminar 22061). In Dagstuhl Reports, Volume 12, Issue 2, pp. 1-16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@Article{gradel_et_al:DagRep.12.2.1,
  author =	{Gr\"{a}del, Erich and Kolaitis, Phokion G. and Noy, Marc and Naaf, Matthias},
  title =	{{Logic and Random Discrete Structures (Dagstuhl Seminar 22061)}},
  pages =	{1--16},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2022},
  volume =	{12},
  number =	{2},
  editor =	{Gr\"{a}del, Erich and Kolaitis, Phokion G. and Noy, Marc and Naaf, Matthias},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DagRep.12.2.1},
  URN =		{urn:nbn:de:0030-drops-169295},
  doi =		{10.4230/DagRep.12.2.1},
  annote =	{Keywords: combinatorics, complexity theory, logic, random structures, probabilistic databases}
}

Document

Track B: Automata, Logic, Semantics, and Theory of Programming

DOI: 10.4230/LIPIcs.ICALP.2021.133

Elementary Equivalence Versus Isomorphism in Semiring Semantics

Authors: Erich Grädel and Lovro Mrkonjić

Published in: LIPIcs, Volume 198, 48th International Colloquium on Automata, Languages, and Programming (ICALP 2021)

Abstract

We study the first-order axiomatisability of finite semiring interpretations or, equivalently, the question whether elementary equivalence and isomorphism coincide for valuations of atomic facts over a finite universe into a commutative semiring. Contrary to the classical case of Boolean semantics, where every finite structure is axiomatised up to isomorphism by a first-order sentence, the situation in semiring semantics is rather different, and depends on the underlying semiring. We prove that for a number of important semirings, including min-max semirings, and the semirings of positive Boolean expressions, there exist finite semiring interpretations that are elementarily equivalent but not isomorphic. The same is true for the polynomial semirings that are universal for the classes of absorptive, idempotent, and fully idempotent semirings, respectively. On the other side, we prove that for other, practically relevant, semirings such as the Viterby semiring 𝕍, the tropical semiring 𝕋, the natural semiring ℕ and the universal polynomial semiring ℕ[X], all finite semiring interpretations are first-order axiomatisable, and thus elementary equivalence implies isomorphism.

Cite as

Erich Grädel and Lovro Mrkonjić. Elementary Equivalence Versus Isomorphism in Semiring Semantics. In 48th International Colloquium on Automata, Languages, and Programming (ICALP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 198, pp. 133:1-133:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{gradel_et_al:LIPIcs.ICALP.2021.133,
  author =	{Gr\"{a}del, Erich and Mrkonji\'{c}, Lovro},
  title =	{{Elementary Equivalence Versus Isomorphism in Semiring Semantics}},
  booktitle =	{48th International Colloquium on Automata, Languages, and Programming (ICALP 2021)},
  pages =	{133:1--133:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-195-5},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{198},
  editor =	{Bansal, Nikhil and Merelli, Emanuela and Worrell, James},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2021.133},
  URN =		{urn:nbn:de:0030-drops-142022},
  doi =		{10.4230/LIPIcs.ICALP.2021.133},
  annote =	{Keywords: Semiring semantics, elementary equivalence, axiomatisability}
}

Document

DOI: 10.4230/LIPIcs.CSL.2021.17

Semiring Provenance for Fixed-Point Logic

Authors: Katrin M. Dannert, Erich Grädel, Matthias Naaf, and Val Tannen

Published in: LIPIcs, Volume 183, 29th EACSL Annual Conference on Computer Science Logic (CSL 2021)

Abstract

Semiring provenance is a successful approach, originating in database theory, to providing detailed information on how atomic facts combine to yield the result of a query. In particular, general provenance semirings of polynomials or formal power series provide precise descriptions of the evaluation strategies or "proof trees" for the query. By evaluating these descriptions in specific application semirings, one can extract practical information for instance about the confidence of a query or the cost of its evaluation. This paper develops semiring provenance for very general logical languages featuring the full interaction between negation and fixed-point inductions or, equivalently, arbitrary interleavings of least and greatest fixed points. This also opens the door to provenance analysis applications for modal μ-calculus and temporal logics, as well as for finite and infinite model-checking games. Interestingly, the common approach based on Kleene’s Fixed-Point Theorem for ω-continuous semirings is not sufficient for these general languages. We show that an adequate framework for the provenance analysis of full fixed-point logics is provided by semirings that are (1) fully continuous, and (2) absorptive. Full continuity guarantees that provenance values of least and greatest fixed-points are well-defined. Absorptive semirings provide a symmetry between least and greatest fixed-points and make sure that provenance values of greatest fixed points are informative. We identify semirings of generalized absorptive polynomials S^{∞}[X] and prove universal properties that make them the most general appropriate semirings for our framework. These semirings have the further property of being (3) chain-positive, which is responsible for having truth-preserving interpretations that give non-zero values to all true formulae. We relate the provenance analysis of fixed-point formulae with provenance values of plays and strategies in the associated model-checking games. Specifically, we prove that the provenance value of a fixed point formula gives precise information on the evaluation strategies in these games.

Cite as

Katrin M. Dannert, Erich Grädel, Matthias Naaf, and Val Tannen. Semiring Provenance for Fixed-Point Logic. In 29th EACSL Annual Conference on Computer Science Logic (CSL 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 183, pp. 17:1-17:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{dannert_et_al:LIPIcs.CSL.2021.17,
  author =	{Dannert, Katrin M. and Gr\"{a}del, Erich and Naaf, Matthias and Tannen, Val},
  title =	{{Semiring Provenance for Fixed-Point Logic}},
  booktitle =	{29th EACSL Annual Conference on Computer Science Logic (CSL 2021)},
  pages =	{17:1--17:22},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-175-7},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{183},
  editor =	{Baier, Christel and Goubault-Larrecq, Jean},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2021.17},
  URN =		{urn:nbn:de:0030-drops-134518},
  doi =		{10.4230/LIPIcs.CSL.2021.17},
  annote =	{Keywords: Finite Model Theory, Semiring Provenance, Absorptive Semirings, Fixed-Point Logics}
}

Document

DOI: 10.4230/LIPIcs.CSL.2020.22

Guarded Teams: The Horizontally Guarded Case

Authors: Erich Grädel and Martin Otto

Published in: LIPIcs, Volume 152, 28th EACSL Annual Conference on Computer Science Logic (CSL 2020)

Abstract

Team semantics admits reasoning about large sets of data, modelled by sets of assignments (called teams), with first-order syntax. This leads to high expressive power and complexity, particularly in the presence of atomic dependency properties for such data sets. It is therefore interesting to explore fragments and variants of logic with team semantics that permit model-theoretic tools and algorithmic methods to control this explosion in expressive power and complexity. We combine here the study of team semantics with the notion of guarded logics, which are well-understood in the case of classical Tarski semantics, and known to strike a good balance between expressive power and algorithmic manageability. In fact there are two strains of guardedness for teams. Horizontal guardedness requires the individual assignments of the team to be guarded in the usual sense of guarded logics. Vertical guardedness, on the other hand, posits an additional (or definable) hypergraph structure on relational structures in order to interpret a constraint on the component-wise variability of assignments within teams. In this paper we investigate the horizontally guarded case. We study horizontally guarded logics for teams and appropriate notions of guarded team bisimulation. In particular, we establish characterisation theorems that relate invariance under guarded team bisimulation with guarded team logics, but also with logics under classical Tarski semantics.

Cite as

Erich Grädel and Martin Otto. Guarded Teams: The Horizontally Guarded Case. In 28th EACSL Annual Conference on Computer Science Logic (CSL 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 152, pp. 22:1-22:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{gradel_et_al:LIPIcs.CSL.2020.22,
  author =	{Gr\"{a}del, Erich and Otto, Martin},
  title =	{{Guarded Teams: The Horizontally Guarded Case}},
  booktitle =	{28th EACSL Annual Conference on Computer Science Logic (CSL 2020)},
  pages =	{22:1--22:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-132-0},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{152},
  editor =	{Fern\'{a}ndez, Maribel and Muscholl, Anca},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2020.22},
  URN =		{urn:nbn:de:0030-drops-116650},
  doi =		{10.4230/LIPIcs.CSL.2020.22},
  annote =	{Keywords: Team semantics, guarded logics, bisimulation, characterisation theorems}
}

Document

DOI: 10.4230/LIPIcs.MFCS.2019.31

Choiceless Logarithmic Space

Authors: Erich Grädel and Svenja Schalthöfer

Published in: LIPIcs, Volume 138, 44th International Symposium on Mathematical Foundations of Computer Science (MFCS 2019)

Abstract

One of the most important open problems in finite model theory is the question whether there is a logic characterising efficient computation. While this question usually concerns Ptime, it can also be applied to other complexity classes, and in particular to Logspace which can be seen as a formalisation of efficient computation for big data. One of the strongest candidates for a logic capturing Ptime is Choiceless Polynomial Time (CPT). It is based on the idea of choiceless algorithms, a general model of symmetric computation over abstract structures (rather than their encodings by finite strings). However, there is currently neither a comparably strong candidate for a logic for Logspace, nor a logic transferring the idea of choiceless computation to Logspace. We propose here a notion of Choiceless Logarithmic Space which overcomes some of the obstacles posed by Logspace as a less robust complexity class. The resulting logic is contained in both Logspace and CPT, and is strictly more expressive than all logics for Logspace that have been known so far. Further, we address the question whether this logic can define all Logspace-queries, and prove that this is not the case.

Cite as

Erich Grädel and Svenja Schalthöfer. Choiceless Logarithmic Space. In 44th International Symposium on Mathematical Foundations of Computer Science (MFCS 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 138, pp. 31:1-31:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{gradel_et_al:LIPIcs.MFCS.2019.31,
  author =	{Gr\"{a}del, Erich and Schalth\"{o}fer, Svenja},
  title =	{{Choiceless Logarithmic Space}},
  booktitle =	{44th International Symposium on Mathematical Foundations of Computer Science (MFCS 2019)},
  pages =	{31:1--31:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-117-7},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{138},
  editor =	{Rossmanith, Peter and Heggernes, Pinar and Katoen, Joost-Pieter},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2019.31},
  URN =		{urn:nbn:de:0030-drops-109758},
  doi =		{10.4230/LIPIcs.MFCS.2019.31},
  annote =	{Keywords: Finite Model Theory, Logics for Logspace, Choiceless Computation}
}

Document

Track B: Automata, Logic, Semantics, and Theory of Programming

DOI: 10.4230/LIPIcs.ICALP.2019.112

Approximations of Isomorphism and Logics with Linear-Algebraic Operators (Track B: Automata, Logic, Semantics, and Theory of Programming)

Authors: Anuj Dawar, Erich Grädel, and Wied Pakusa

Published in: LIPIcs, Volume 132, 46th International Colloquium on Automata, Languages, and Programming (ICALP 2019)

Abstract

Invertible map equivalences are approximations of graph isomorphism that refine the well-known Weisfeiler-Leman method. They are parameterized by a number k and a set Q of primes. The intuition is that two equivalent graphs G equiv^IM_{k, Q} H cannot be distinguished by means of partitioning the set of k-tuples in both graphs with respect to any linear-algebraic operator acting on vector spaces over fields of characteristic p, for any p in Q. These equivalences have first appeared in the study of rank logic, but in fact they can be used to delimit the expressive power of any extension of fixed-point logic with linear-algebraic operators. We define {LA^{k}}(Q), an infinitary logic with k variables and all linear-algebraic operators over finite vector spaces of characteristic p in Q and show that equiv^IM_{k, Q} is the natural notion of elementary equivalence for this logic. The logic LA^{omega}(Q) = Cup_{k in omega} LA^{k}(Q) is then a natural upper bound on the expressive power of any extension of fixed-point logics by means of Q-linear-algebraic operators. By means of a new and much deeper algebraic analysis of a generalized variant, for any prime p, of the CFI-structures due to Cai, Fürer, and Immerman, we prove that, as long as Q is not the set of all primes, there is no k such that equiv^IM_{k, Q} is the same as isomorphism. It follows that there are polynomial-time properties of graphs which are not definable in LA^{omega}(Q), which implies that no extension of fixed-point logic with linear-algebraic operators can capture PTIME, unless it includes such operators for all prime characteristics. Our analysis requires substantial algebraic machinery, including a homogeneity property of CFI-structures and Maschke’s Theorem, an important result from the representation theory of finite groups.

Cite as

Anuj Dawar, Erich Grädel, and Wied Pakusa. Approximations of Isomorphism and Logics with Linear-Algebraic Operators (Track B: Automata, Logic, Semantics, and Theory of Programming). In 46th International Colloquium on Automata, Languages, and Programming (ICALP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 132, pp. 112:1-112:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{dawar_et_al:LIPIcs.ICALP.2019.112,
  author =	{Dawar, Anuj and Gr\"{a}del, Erich and Pakusa, Wied},
  title =	{{Approximations of Isomorphism and Logics with Linear-Algebraic Operators}},
  booktitle =	{46th International Colloquium on Automata, Languages, and Programming (ICALP 2019)},
  pages =	{112:1--112:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-109-2},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{132},
  editor =	{Baier, Christel and Chatzigiannakis, Ioannis and Flocchini, Paola and Leonardi, Stefano},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2019.112},
  URN =		{urn:nbn:de:0030-drops-106887},
  doi =		{10.4230/LIPIcs.ICALP.2019.112},
  annote =	{Keywords: Finite Model Theory, Graph Isomorphism, Descriptive Complexity, Algebra}
}

Document

DOI: 10.4230/DagRep.9.1.28

Logics for Dependence and Independence (Dagstuhl Seminar 19031)

Authors: Erich Grädel, Phokion G. Kolaitis, Juha Kontinen, and Heribert Vollmer

Published in: Dagstuhl Reports, Volume 9, Issue 1 (2019)

Abstract

This report documents the programme and outcomes of Dagstuhl Seminar 19031 "Logics for Dependence and Independence". This seminar served as a follow-up seminar to the highly successful seminars "Dependence Logic: Theory and Applications" (13071) and "Logics for Dependence and Independence" (15261). A key objective of the seminar was to bring together researchers working in dependence logic and in the application areas so that they can communicate state-of-the-art advances and embark on a systematic interaction. The goal was especially to reach those researchers who have recently started working in this thriving area as well as researchers working on several aspects of database theory, separation logic, and logics of uncertainy.

Cite as

Erich Grädel, Phokion G. Kolaitis, Juha Kontinen, and Heribert Vollmer. Logics for Dependence and Independence (Dagstuhl Seminar 19031). In Dagstuhl Reports, Volume 9, Issue 1, pp. 28-46, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@Article{gradel_et_al:DagRep.9.1.28,
  author =	{Gr\"{a}del, Erich and Kolaitis, Phokion G. and Kontinen, Juha and Vollmer, Heribert},
  title =	{{Logics for Dependence and Independence (Dagstuhl Seminar 19031)}},
  pages =	{28--46},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2019},
  volume =	{9},
  number =	{1},
  editor =	{Gr\"{a}del, Erich and Kolaitis, Phokion G. and Kontinen, Juha and Vollmer, Heribert},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DagRep.9.1.28},
  URN =		{urn:nbn:de:0030-drops-105682},
  doi =		{10.4230/DagRep.9.1.28},
  annote =	{Keywords: dependence logic, mathematical logic, computational complexity, finite model theory, game theory}
}

Document

DOI: 10.4230/LIPIcs.CSL.2018.25

Dependency Concepts up to Equivalence

Authors: Erich Grädel and Matthias Hoelzel

Published in: LIPIcs, Volume 119, 27th EACSL Annual Conference on Computer Science Logic (CSL 2018)

Abstract

Modern logics of dependence and independence are based on different variants of atomic dependency statements (such as dependence, exclusion, inclusion, or independence) and on team semantics: A formula is evaluated not with a single assignment of values to the free variables, but with a set of such assignments, called a team. In this paper we explore logics of dependence and independence where the atomic dependency statements cannot distinguish elements up to equality, but only up to a given equivalence relation (which may model observational indistinguishabilities, for instance between states of a computational process or between values obtained in an experiment). Our main goal is to analyse the power of such logics, by identifying equally expressive fragments of existential second-order logic or greatest fixed-point logic, with relations that are closed under the given equivalence. Using an adaptation of the Ehrenfeucht-Fraïssé method we further study conditions on the given equivalences under which these logics collapse to first-order logic, are equivalent to full existential second-order logic, or are strictly between first-order and existential second-order logic.

Cite as

Erich Grädel and Matthias Hoelzel. Dependency Concepts up to Equivalence. In 27th EACSL Annual Conference on Computer Science Logic (CSL 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 119, pp. 25:1-25:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{gradel_et_al:LIPIcs.CSL.2018.25,
  author =	{Gr\"{a}del, Erich and Hoelzel, Matthias},
  title =	{{Dependency Concepts up to Equivalence}},
  booktitle =	{27th EACSL Annual Conference on Computer Science Logic (CSL 2018)},
  pages =	{25:1--25:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-088-0},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{119},
  editor =	{Ghica, Dan R. and Jung, Achim},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2018.25},
  URN =		{urn:nbn:de:0030-drops-96921},
  doi =		{10.4230/LIPIcs.CSL.2018.25},
  annote =	{Keywords: Logics of dependence and independence, Team semantics, Existential second-order logic, Observational equivalence, Expressive power}
}

Document

DOI: 10.4230/DagRep.7.9.1

Finite and Algorithmic Model Theory (Dagstuhl Seminar 17361)

Authors: Anuj Dawar, Erich Grädel, Phokion G. Kolaitis, and Thomas Schwentick

Published in: Dagstuhl Reports, Volume 7, Issue 9 (2018)

Abstract

This report documents the program and the outcomes of Dagstuhl Seminar 17361 "Finite and Algorithmic Model Theory".

Cite as

Anuj Dawar, Erich Grädel, Phokion G. Kolaitis, and Thomas Schwentick. Finite and Algorithmic Model Theory (Dagstuhl Seminar 17361). In Dagstuhl Reports, Volume 7, Issue 9, pp. 1-25, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@Article{dawar_et_al:DagRep.7.9.1,
  author =	{Dawar, Anuj and Gr\"{a}del, Erich and Kolaitis, Phokion G. and Schwentick, Thomas},
  title =	{{Finite and Algorithmic Model Theory (Dagstuhl Seminar 17361)}},
  pages =	{1--25},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2018},
  volume =	{7},
  number =	{9},
  editor =	{Dawar, Anuj and Gr\"{a}del, Erich and Kolaitis, Phokion G. and Schwentick, Thomas},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DagRep.7.9.1},
  URN =		{urn:nbn:de:0030-drops-85863},
  doi =		{10.4230/DagRep.7.9.1},
  annote =	{Keywords: algorithms, database theory, descriptive complexity, finite model theory, independence logic, knowledge representation, model checking}
}

Document

DOI: 10.4230/LIPIcs.CSL.2017.27

The Model-Theoretic Expressiveness of Propositional Proof Systems

Authors: Erich Grädel, Benedikt Pago, and Wied Pakusa

Published in: LIPIcs, Volume 82, 26th EACSL Annual Conference on Computer Science Logic (CSL 2017)

Abstract

We establish new, and surprisingly tight, connections between propositional proof complexity and finite model theory. Specifically, we show that the power of several propositional proof systems, such as Horn resolution, bounded width resolution, and the polynomial calculus of bounded degree, can be characterised in a precise sense by variants of fixed-point logics that are of fundamental importance in descriptive complexity theory. Our main results are that Horn resolution has the same expressive power as least fixed-point logic, that bounded width resolution captures existential least fixed-point logic, and that the (monomial restriction of the) polynomial calculus of bounded degree solves precisely the problems definable in fixed-point logic with counting.

Cite as

Erich Grädel, Benedikt Pago, and Wied Pakusa. The Model-Theoretic Expressiveness of Propositional Proof Systems. In 26th EACSL Annual Conference on Computer Science Logic (CSL 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 82, pp. 27:1-27:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{gradel_et_al:LIPIcs.CSL.2017.27,
  author =	{Gr\"{a}del, Erich and Pago, Benedikt and Pakusa, Wied},
  title =	{{The Model-Theoretic Expressiveness of Propositional Proof Systems}},
  booktitle =	{26th EACSL Annual Conference on Computer Science Logic (CSL 2017)},
  pages =	{27:1--27:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-045-3},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{82},
  editor =	{Goranko, Valentin and Dam, Mads},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2017.27},
  URN =		{urn:nbn:de:0030-drops-76897},
  doi =		{10.4230/LIPIcs.CSL.2017.27},
  annote =	{Keywords: Propositional proof systems, fixed-point logics, resolution, polynomial calculus, generalized quantifiers}
}

Document

DOI: 10.4230/LIPIcs.CSL.2017.35

Advice Automatic Structures and Uniformly Automatic Classes

Authors: Faried Abu Zaid, Erich Grädel, and Frederic Reinhardt

Published in: LIPIcs, Volume 82, 26th EACSL Annual Conference on Computer Science Logic (CSL 2017)

Abstract

We study structures that are automatic with advice. These are structures that admit a presentation by finite automata (over finite or infinite words or trees) with access to an additional input,called an advice. Over finite words, a standard example of a structure that is automatic with advice, but not automatic in the classical sense, is the additive group of rational numbers (Q,+). By using a set of advices rather than a single advice, this leads to the new concept of a parameterised automatic presentation as a means to uniformly represent a whole class of structures. The decidability of the first-order theory of such a uniformly automatic class reduces to the decidability of the monadic second-order theory of the set of advices that are used in the presentation. Such decidability results also hold for extensions of first-order logic by regularity preserving quantifiers, such as cardinality quantifiers and Ramsey quantifiers. To investigate the power of this concept, we present examples of structures and classes of structures that are automatic with advice but not without advice, and we prove classification theorems for the structures with an advice automatic presentation for several algebraic domains. In particular, we prove that the class of all torsion-free Abelian groups of rank one is uniformly omega-automatic and that there is a uniform omega-tree-automatic presentation of the class of all Abelian groups up to elementary equivalence and of the class of all countable divisible Abelian groups. On the other hand we show that every uniformly omega-automatic class of Abelian groups must have bounded rank. While for certain domains, such as trees and Abelian groups, it turns out that automatic presentations with advice are capable of presenting significantly more complex structures than ordinary automatic presentations, there are other domains, such as Boolean algebras, where this is provably not the case. Further, advice seems to not be of much help for representing some particularly relevant examples of structures with decidable theories, most notably the field of reals. Finally we study closure properties for several kinds of uniformly automatic classes, and decision problems concerning the number of non-isomorphic models in uniformly automatic classes with the unique representation property.

Cite as

Faried Abu Zaid, Erich Grädel, and Frederic Reinhardt. Advice Automatic Structures and Uniformly Automatic Classes. In 26th EACSL Annual Conference on Computer Science Logic (CSL 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 82, pp. 35:1-35:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{abuzaid_et_al:LIPIcs.CSL.2017.35,
  author =	{Abu Zaid, Faried and Gr\"{a}del, Erich and Reinhardt, Frederic},
  title =	{{Advice Automatic Structures and Uniformly Automatic Classes}},
  booktitle =	{26th EACSL Annual Conference on Computer Science Logic (CSL 2017)},
  pages =	{35:1--35:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-045-3},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{82},
  editor =	{Goranko, Valentin and Dam, Mads},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2017.35},
  URN =		{urn:nbn:de:0030-drops-76971},
  doi =		{10.4230/LIPIcs.CSL.2017.35},
  annote =	{Keywords: automatic structures, algorithmic model theory, decidable theories, torsion-free abelian groups, first-order logic}
}

Document

DOI: 10.4230/LIPIcs.CSL.2016.35

Counting in Team Semantics

Authors: Erich Grädel and Stefan Hegselmann

Published in: LIPIcs, Volume 62, 25th EACSL Annual Conference on Computer Science Logic (CSL 2016)

Abstract

We explore several counting constructs for logics with team semantics. Counting is an important task in numerous applications, but with a somewhat delicate relationship to logic. Team semantics on the other side is the mathematical basis of modern logics of dependence and independence, in which formulae are evaluated not for a single assignment of values to variables, but for a set of such assignments. It is therefore interesting to ask what kind of counting constructs are adequate in this context, and how such constructs influence the expressive power, and the model-theoretic and algorithmic properties of logics with team semantics. Due to the second-order features of team semantics there is a rich variety of potential counting constructs. Here we study variations of two main ideas: forking atoms and counting quantifiers. Forking counts how many different values for a tuple w occur in assignments with coinciding values for v. We call this the forking degree of bar v with respect to bar w. Forking is powerful enough to capture many of the previously studied atomic dependency properties. In particular we exhibit logics with forking atoms that have, respectively, precisely the power of dependence logic and independence logic. Our second approach uses counting quantifiers E^{geq mu} of a similar kind as used in logics with Tarski semantics. The difference is that these quantifiers are now applied to teams of assignments that may give different values to mu. We show that, on finite structures, there is an intimate connection between inclusion logic with counting quantifiers and FPC, fixed-point logic with counting, which is a logic of fundamental importance for descriptive complexity theory. For sentences, the two logics have the same expressive power. Our analysis is based on a new variant of model-checking games, called threshold safety games, on a trap condition for such games, and on game interpretations.

Cite as

Erich Grädel and Stefan Hegselmann. Counting in Team Semantics. In 25th EACSL Annual Conference on Computer Science Logic (CSL 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 62, pp. 35:1-35:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{gradel_et_al:LIPIcs.CSL.2016.35,
  author =	{Gr\"{a}del, Erich and Hegselmann, Stefan},
  title =	{{Counting in Team Semantics}},
  booktitle =	{25th EACSL Annual Conference on Computer Science Logic (CSL 2016)},
  pages =	{35:1--35:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-022-4},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{62},
  editor =	{Talbot, Jean-Marc and Regnier, Laurent},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2016.35},
  URN =		{urn:nbn:de:0030-drops-65757},
  doi =		{10.4230/LIPIcs.CSL.2016.35},
  annote =	{Keywords: logics with counting, team semantics, fixed-point logic with counting}
}

Document

DOI: 10.4230/DagRep.5.6.70

Logics for Dependence and Independence (Dagstuhl Seminar 15261)

Authors: Erich Grädel, Juha Kontinen, Jouka Väänänen, and Heribert Vollmer

Published in: Dagstuhl Reports, Volume 5, Issue 6 (2016)

Abstract

This report documents the programme and outcomes of Dagstuhl Seminar 15261 "Logics for Dependence and Independence". This seminar served as a follow-up seminar to the highly successful seminar "Dependence Logic: Theory and Applications" (Dagstuhl Seminar 13071). A key objective of the seminar was to bring together researchers working in dependence logic and in the application areas so that they can communicate state-of-the-art advances and embark on a systematic interaction. The goal was especially to reach those researchers who have recently started working in this thriving area.

Cite as

Erich Grädel, Juha Kontinen, Jouka Väänänen, and Heribert Vollmer. Logics for Dependence and Independence (Dagstuhl Seminar 15261). In Dagstuhl Reports, Volume 5, Issue 6, pp. 70-85, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@Article{gradel_et_al:DagRep.5.6.70,
  author =	{Gr\"{a}del, Erich and Kontinen, Juha and V\"{a}\"{a}n\"{a}nen, Jouka and Vollmer, Heribert},
  title =	{{Logics for Dependence and Independence (Dagstuhl Seminar 15261)}},
  pages =	{70--85},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2016},
  volume =	{5},
  number =	{6},
  editor =	{Gr\"{a}del, Erich and Kontinen, Juha and V\"{a}\"{a}n\"{a}nen, Jouka and Vollmer, Heribert},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DagRep.5.6.70},
  URN =		{urn:nbn:de:0030-drops-55084},
  doi =		{10.4230/DagRep.5.6.70},
  annote =	{Keywords: team semantics, dependence logic, mathematical logic, computational complexity, finite model theory, game theory}
}

Document

DOI: 10.4230/LIPIcs.CSL.2015.390

Rank Logic is Dead, Long Live Rank Logic!

Authors: Erich Grädel and Wied Pakusa

Published in: LIPIcs, Volume 41, 24th EACSL Annual Conference on Computer Science Logic (CSL 2015)

Abstract

Motivated by the search for a logic for polynomial time, we study rank logic (FPR) which extends fixed-point logic with counting (FPC) by operators that determine the rank of matrices over finite fields. While FPR can express most of the known queries that separate FPC from PTIME, nearly nothing was known about the limitations of its expressive power. In our first main result we show that the extensions of FPC by rank operators over different prime fields are incomparable. This solves an open question posed by Dawar and Holm and also implies that rank logic, in its original definition with a distinct rank operator for every field, fails to capture polynomial time. In particular we show that the variant of rank logic FPR* with an operator that uniformly expresses the matrix rank over finite fields is more expressive than FPR. One important step in our proof is to consider solvability logic FPS which is the analogous extension of FPC by quantifiers which express the solvability problem for linear equation systems over finite fields. Solvability logic can easily be embedded into rank logic, but it is open whether it is a strict fragment. In our second main result we give a partial answer to this question: in the absence of counting, rank operators are strictly more expressive than solvability quantifiers.

Cite as

Erich Grädel and Wied Pakusa. Rank Logic is Dead, Long Live Rank Logic!. In 24th EACSL Annual Conference on Computer Science Logic (CSL 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 41, pp. 390-404, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{gradel_et_al:LIPIcs.CSL.2015.390,
  author =	{Gr\"{a}del, Erich and Pakusa, Wied},
  title =	{{Rank Logic is Dead, Long Live Rank Logic!}},
  booktitle =	{24th EACSL Annual Conference on Computer Science Logic (CSL 2015)},
  pages =	{390--404},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-90-3},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{41},
  editor =	{Kreutzer, Stephan},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2015.390},
  URN =		{urn:nbn:de:0030-drops-54279},
  doi =		{10.4230/LIPIcs.CSL.2015.390},
  annote =	{Keywords: logic, descriptive complexity, polynomial time, rank logic}
}

Document

DOI: 10.4230/LIPIcs.CSL.2012.213

Definability of linear equation systems over groups and rings

Authors: Anuj Dawar, Erich Grädel, Bjarki Holm, Eryk Kopczynski, and Wied Pakusa

Published in: LIPIcs, Volume 16, Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL (2012)

Abstract

Motivated by the quest for a logic for PTIME and recent insights that the descriptive complexity of problems from linear algebra is a crucial aspect of this problem, we study the solvability of linear equation systems over finite groups and rings from the viewpoint of logical (inter-)definability. All problems that we consider are decidable in polynomial time, but not expressible in fixed-point logic with counting. They also provide natural candidates for a separation of polynomial time from rank logics, which extend fixed-point logics by operators for determining the rank of definable matrices and which are sufficient for solvability problems over fields. Based on the structure theory of finite rings, we establish logical reductions among various solvability problems. Our results indicate that all solvability problems for linear equation systems that separate fixed-point logic with counting from PTIME can be reduced to solvability over commutative rings. Further, we prove closure properties for classes of queries that reduce to solvability over rings. As an application, these closure properties provide normal forms for logics extended with solvability operators.

Cite as

Anuj Dawar, Erich Grädel, Bjarki Holm, Eryk Kopczynski, and Wied Pakusa. Definability of linear equation systems over groups and rings. In Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL. Leibniz International Proceedings in Informatics (LIPIcs), Volume 16, pp. 213-227, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2012)

Copy BibTex To Clipboard

@InProceedings{dawar_et_al:LIPIcs.CSL.2012.213,
  author =	{Dawar, Anuj and Gr\"{a}del, Erich and Holm, Bjarki and Kopczynski, Eryk and Pakusa, Wied},
  title =	{{Definability of linear equation systems over groups and rings}},
  booktitle =	{Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL},
  pages =	{213--227},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-42-2},
  ISSN =	{1868-8969},
  year =	{2012},
  volume =	{16},
  editor =	{C\'{e}gielski, Patrick and Durand, Arnaud},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2012.213},
  URN =		{urn:nbn:de:0030-drops-36749},
  doi =		{10.4230/LIPIcs.CSL.2012.213},
  annote =	{Keywords: inite model theory, logics with algebraic operators}
}

Document

DOI: 10.4230/LIPIcs.CSL.2012.305

Banach-Mazur Games with Simple Winning Strategies

Authors: Erich Grädel and Simon Leßenich

Published in: LIPIcs, Volume 16, Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL (2012)

Abstract

We discuss several notions of "simple" winning strategies for Banach-Mazur games on graphs, such as positional strategies, move-counting or length-counting strategies, and strategies with a memory based on finite appearance records (FAR). We investigate classes of Banach-Mazur games that are determined via these kinds of winning strategies. Banach-Mazur games admit stronger determinacy results than classical graph games. For instance, all Banach-Mazur games with omega-regular winning conditions are positionally determined. Beyond the omega-regular winning conditions, we focus here on Muller conditions with infinitely many colours. We investigate the infinitary Muller conditions that guarantee positional determinacy for Banach-Mazur games. Further, we determine classes of such conditions that require infinite memory but guarantee determinacy via move-counting strategies, length-counting strategies, and FAR-strategies. We also discuss the relationships between these different notions of determinacy.

Cite as

Erich Grädel and Simon Leßenich. Banach-Mazur Games with Simple Winning Strategies. In Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL. Leibniz International Proceedings in Informatics (LIPIcs), Volume 16, pp. 305-319, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2012)

Copy BibTex To Clipboard

@InProceedings{gradel_et_al:LIPIcs.CSL.2012.305,
  author =	{Gr\"{a}del, Erich and Le{\ss}enich, Simon},
  title =	{{Banach-Mazur Games with Simple Winning Strategies}},
  booktitle =	{Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL},
  pages =	{305--319},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-42-2},
  ISSN =	{1868-8969},
  year =	{2012},
  volume =	{16},
  editor =	{C\'{e}gielski, Patrick and Durand, Arnaud},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2012.305},
  URN =		{urn:nbn:de:0030-drops-36806},
  doi =		{10.4230/LIPIcs.CSL.2012.305},
  annote =	{Keywords: Banach-Mazur games, winning strategies, positional determinacy, Muller winning conditions}
}

Document

DOI: 10.4230/LIPIcs.STACS.2012.577

The Field of Reals is not omega-Automatic

Authors: Faried Abu Zaid, Erich Grädel, and Lukasz Kaiser

Published in: LIPIcs, Volume 14, 29th International Symposium on Theoretical Aspects of Computer Science (STACS 2012)

Abstract

We investigate structural properties of omega-automatic presentations of infinite structures in order to sharpen our methods to determine whether a given structure is omega-automatic. We apply these methods to show that no field of characteristic 0 admits an injective omega-automatic presentation, and that uncountable fields with a definable linear order cannot be omega-automatic.

Cite as

Faried Abu Zaid, Erich Grädel, and Lukasz Kaiser. The Field of Reals is not omega-Automatic. In 29th International Symposium on Theoretical Aspects of Computer Science (STACS 2012). Leibniz International Proceedings in Informatics (LIPIcs), Volume 14, pp. 577-588, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2012)

Copy BibTex To Clipboard

@InProceedings{abuzaid_et_al:LIPIcs.STACS.2012.577,
  author =	{Abu Zaid, Faried and Gr\"{a}del, Erich and Kaiser, Lukasz},
  title =	{{The Field of Reals is not omega-Automatic}},
  booktitle =	{29th International Symposium on Theoretical Aspects of Computer Science (STACS 2012)},
  pages =	{577--588},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-35-4},
  ISSN =	{1868-8969},
  year =	{2012},
  volume =	{14},
  editor =	{D\"{u}rr, Christoph and Wilke, Thomas},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2012.577},
  URN =		{urn:nbn:de:0030-drops-34234},
  doi =		{10.4230/LIPIcs.STACS.2012.577},
  annote =	{Keywords: Logic, Algorithmic Model Theory, Automatic Structures}
}

Document

DOI: 10.4230/LIPIcs.STACS.2008.1352

Model Checking Games for the Quantitative µ-Calculus

Authors: Diana Fischer, Erich Grädel, and Lukasz Kaiser

Published in: LIPIcs, Volume 1, 25th International Symposium on Theoretical Aspects of Computer Science (2008)

Abstract

We investigate quantitative extensions of modal logic and the modal $mu$-calculus, and study the question whether the tight connection between logic and games can be lifted from the qualitative logics to their quantitative counterparts. It turns out that, if the quantitative $mu$-calculus is defined in an appropriate way respecting the duality properties between the logical operators, then its model checking problem can indeed be characterised by a quantitative variant of parity games. However, these quantitative games have quite different properties than their classical counterparts, in particular they are, in general, not positionally determined. The correspondence between the logic and the games goes both ways: the value of a formula on a quantitative transition system coincides with the value of the associated quantitative game, and conversely, the values of quantitative parity games are definable in the quantitative $mu$-calculus.

Cite as

Diana Fischer, Erich Grädel, and Lukasz Kaiser. Model Checking Games for the Quantitative µ-Calculus. In 25th International Symposium on Theoretical Aspects of Computer Science. Leibniz International Proceedings in Informatics (LIPIcs), Volume 1, pp. 301-312, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2008)

Copy BibTex To Clipboard

@InProceedings{fischer_et_al:LIPIcs.STACS.2008.1352,
  author =	{Fischer, Diana and Gr\"{a}del, Erich and Kaiser, Lukasz},
  title =	{{Model Checking Games for the Quantitative µ-Calculus}},
  booktitle =	{25th International Symposium on Theoretical Aspects of Computer Science},
  pages =	{301--312},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-06-4},
  ISSN =	{1868-8969},
  year =	{2008},
  volume =	{1},
  editor =	{Albers, Susanne and Weil, Pascal},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2008.1352},
  URN =		{urn:nbn:de:0030-drops-13525},
  doi =		{10.4230/LIPIcs.STACS.2008.1352},
  annote =	{Keywords: Games, logic, model checking, quantitative logics}
}

Document

DOI: 10.4230/DagSemRep.253

Finite Model Theory, Databases, and Computer-Aided Verification (Dagstuhl Seminar 99401)

Authors: Georg Gottlob, Erich Grädel, Moshe Vardi, and Victor Vianu

Published in: Dagstuhl Seminar Reports. Dagstuhl Seminar Reports, Volume 1 (2021)

Abstract

Cite as

Georg Gottlob, Erich Grädel, Moshe Vardi, and Victor Vianu. Finite Model Theory, Databases, and Computer-Aided Verification (Dagstuhl Seminar 99401). Dagstuhl Seminar Report 253, pp. 1-25, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2000)

Copy BibTex To Clipboard

@TechReport{gottlob_et_al:DagSemRep.253,
  author =	{Gottlob, Georg and Gr\"{a}del, Erich and Vardi, Moshe and Vianu, Victor},
  title =	{{Finite Model Theory, Databases, and Computer-Aided Verification (Dagstuhl Seminar 99401)}},
  pages =	{1--25},
  ISSN =	{1619-0203},
  year =	{2000},
  type = 	{Dagstuhl Seminar Report},
  number =	{253},
  institution =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DagSemRep.253},
  URN =		{urn:nbn:de:0030-drops-151399},
  doi =		{10.4230/DagSemRep.253},
}

Search Results

Documents authored by Grädel, Erich

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Thanks for your feedback!

Could not send message